$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $A$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$;${\it da}$).
\\[0ex]ecl{-}trans{-}act(${\it ds}$;${\it da}$;$A$) $\in$ $\mathbb{N}\rightarrow$(event{-}info(${\it ds}$;${\it da}$) List)$\rightarrow$Prop